Multi-lifts System Example

Multi-lifts System Example

Muti-lift systems heavily rely on control software. Even though they have been used as a typical case study in software engineering research communities, the combination of real-time and probability have never been considered before. A multi-lift system consists of many components, e.g., multiple lifts, floors, internal and external button panels, etc. It is complex in control logic as behavior of different components must be coordinated through a software controller. The system has non-trivial data components and data operations, e.g., maintaining queues for internal and external requests. It depends on quantitative timing, e.g., a lift travels/reacts at limited speed.

We model a lift system check what the probability is for a user is "ignored" by the system, which means a user has requested to travel in certain direction, but a lift passes by, traveling in the same direction without letting the user in. Following is the model.

#import "PAT.Lib.Lift";
#define NoOfFloors 2;
#define NoOfLifts 2;
var<LiftControl> ctrl = new LiftControl(NoOfFloors,NoOfLifts);
var passby = 0;

We difine a external C# library which includes all the functions controlling the lift system. Passby records if a user is be ignored by a lift. 0 means no and 1 means yes.

aSystem = (||| x:{0..NoOfLifts-1} @ Lift(x, 0, 1)) ||| Requests();
Requests() = Request();Request();
Request() = pcase {
                                          1: extreq.0.1{ctrl.AssignExternalRequest(0,1)} -> Skip
                                          1 : intreq.0.0.1{ctrl.AddInternalRequest(0,0)} -> Skip
                                          1 : intreq.1.0.1{ctrl.AddInternalRequest(1,0)} -> Skip
                                         1 : extreq.1.0{ctrl.AssignExternalRequest(1,0)} -> Skip
                                         1 : intreq.0.1.1{ctrl.AddInternalRequest(0,1)} -> Skip
                                        1 : intreq.1.1.1{ctrl.AddInternalRequest(1,1)} -> Skip
                                      } within[1];
Lift(i, level, direction) = case {
            ctrl.isToOpenDoor(i, level) == 1 : (serve.level.direction{ctrl.ClearRequests(i, level, direction)} -> Lift(i, level, direction))
            ctrl.KeepMoving(i, level, direction) == 1 : (reach.level+direction.direction{passby = ctrl.UpdateLiftStatus(i, level, direction)} -> Lift(i, level+direction, direction))
            ctrl.HasAssignment(i) == 1 : changedirection.i{ctrl.ChangeDirection(i)} -> Lift(i, level, -1*direction)
            default : idle.i -> Lift(i, level, direction)
       } within[2];

Finally we define the goal we need.

#define goal passby == 1;
#assert aSystem reaches goal with prob;